The design and testing of software is often an expensive and time-consuming process. Tools based on model checking with automaton specifications have been very effective at finding important bugs such as buffer overflows, memory safety violations, and violations of locking and security policies. Static analysis tools and model checking tools are typically based on inter-procedural algorithms for propagating dataflow information. These algorithms perform a reachability analysis that generally starts from scratch. For small program changes, however, which typically have only a localized effect on the analysis, a non-incremental (“from scratch”) approach can be inefficient.
At least one technique has been proposed or suggested for the incremental evaluation of logic programs. See, D. Saha and C. Ramakrishnan, Incremental Evaluation of Tabled Logic Programs, ICLP, 392-406, Mumbai, India (2003); or D. Saha and C. Ramakrishnan, Incremental and Demand Driven Points-to Analysis Using Logic Programming, Principles and Practice of Declarative Programming (2005). Several program analysis problems can be cast as a logic program. Incremental program analyzers are disclosed that compute the changes to the analysis information due to small changes in the input program rather than reanalyzing the entire program. The disclosed incremental program analyzers operate in the forward direction from the initial states.
While such incremental program analyzers can effectively compute the changes to analysis information due to small changes in the input program, they suffer from a number of limitations, which if overcome, could further improve the utility and efficiency of incremental program evaluation techniques. For example, such forward incremental analysis techniques reanalyze portions of the program, leading to inefficiencies. In addition, prior incremental program analyzers require translation of software programs, such as C++ programs, to logic programs, leading to further inefficiencies.
A need therefore exists for incremental algorithms for inter-procedural analysis that operate in a backward direction, “inside-out” from the locations of the program changes.